function deserialize_file(file) {
  document.getElementById("inp_command").value = "deserialize_file";
  document.getElementById("inp_file").value = file;
  document.getElementById("frm_deserializer").submit();
}